\def\CTeXPreproc{Created by ctex v0.2.12, don't edit!}
\documentclass[runningheads]{ctextemp_llncs}
\usepackage{stmaryrd}
\usepackage{amsfonts}

\usepackage{amssymb}
\setcounter{tocdepth}{3}
\usepackage{graphicx}
\usepackage{ctextemp_algorithmic,ctextemp_algorithm}

\usepackage{url}
\newcommand{\keywords}[1]{\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}

\begin{document}

\mainmatter  % start of an individual contribution

% first the title is needed
\title{Modeling and Verification of PLC Timers in Coq}

% a short form should be given in case it is too long for the running head
\titlerunning{Modeling and Verification of PLC Timers in Coq}

% the name(s) of the author(s) follow(s) next
%
% NB: Chinese authors should write their first names(s) in front of
% their surnames. This ensures that the names appear correctly in
% the running heads and the author index.
%
\author{}
%
\authorrunning{}
% (feature abused for this document to repeat the title also on left hand pages)

% the affiliations are given next; don't give your e-mail address
% unless you accept that it will be published
\institute{}

\toctitle{} \tocauthor{} \maketitle


\begin{abstract}



\keywords{PLC, Coq, TON-Timer}
\end{abstract}

\section{Introduction}

\section{Timers in PLC}

According to 

\section{Modeling Timers in PLC}

\subsection{Modeling Scan Cycle}

\subsection{Modeling Relays}

\subsection{Modeling Timers}

\section{Case Study}

\section{Conclusions}

\bibliographystyle{splncs}
\bibliography{ref}

\end{document}
